(** ** Matrix Addition Properties *)
Require Export List.
Require Export Matrix.list_function.
Require Export Matrix.Mat_def.
Require Export Matrix.Mat_IO.
Require Export Matrix.Mat_map.
Import ListNotations.

(* ################################################################# *)

(** This section separately proves various properties of matrix
    addition, including commutation law, associativity law, left plus
    zero matrix property and right plus zero matrix property. *)

Section add_lemma.
Variable A:Set.
Variable Zero:A.
Variable add:A->A->A.


(** * Matrix Addition Commutative Law *)

(** *** matrix_each'_comm *)
(** The addition of two-dimensional lists addition has the property of
    commutative law : ma+mb = mb+ma. *)
Lemma matrix_each'_comm: forall (m n :nat)(left right:list (list A)),
  (forall a b : A, add a b = add b a)->
  height left = m -> height right = m ->
  width left n -> width right n ->
  mat_each' A add left right = mat_each' A add right left.
Proof.
  induction m.
  induction left.
  induction right.
  - simpl. auto.
  - simpl. auto.
  - intros. inversion H0.
  - induction left. induction right.
    + simpl. auto.
    + simpl. auto.
    + induction right.
      { simpl. auto. }
      { intros. simpl. f_equal.  apply list_each_comm with (n:=n) . 
        inversion H2. auto. inversion H2. auto. inversion H3. auto. 
        apply IHm with(n:=n). auto. inversion H0. auto. inversion H1. auto. 
        inversion H2. auto. inversion H3. auto. }
Qed.

(** ** matrix_comm *)
(** The addition of matrices has the property of commutative law : 
    A + B = B + A. *)
Lemma matrix_comm : forall {m n:nat}(left right:@Mat A m n) ,
  (forall a b : A, add a b = add b a) -> 
  matrix_each A add left right === matrix_each A add right left.
Proof.
  intros m n.
  induction left.
  - induction right.
    + intros. unfold matrix_each. 
      unfold mat_each. simpl.
      unfold M_eq. simpl.
      apply matrix_each'_comm with(m:=m) (n:=n).
      apply H. apply mat_height. apply mat_height0.
      apply mat_width. apply mat_width0.
Qed.

(** * Matrix Addition Associative Law *)

(** *** matrix_each'_assoc *)
(** The addition of two-dimensional lists has the property of 
    association law : ma + mb + mc = ma + ( mb + mc ). *)
Lemma matrix_each'_assoc: forall(n m:nat) left middle right ,
  (forall a b c: A, add (add a b) c = add a (add b c))->
  height left = m -> height middle = m ->height right = m -> 
  width left n -> width middle n -> width right n -> 
  mat_each' A add (mat_each' A add left middle) right 
  = mat_each' A add left (mat_each' A add middle right).
Proof.
  intros n.
  induction m.
  induction left.
  induction middle.
  induction right.
  - simpl. auto.
  - simpl. auto.
  - simpl. intros. auto.
  - intros. inversion H0.
  - induction left. induction middle. induction right.
    + simpl. auto.
    + simpl. auto.
    + simpl. auto.
    + induction middle. induction right.
      { simpl. auto. } { simpl. auto. } 
      { induction right. 
        * simpl. auto.
        * simpl. intros. rewrite list_each_assoc with(n:=n). 
          rewrite IHm;auto. destruct H3. auto. destruct H4. auto. 
          destruct H5. auto. auto. destruct H3. auto. destruct H4. 
          auto. destruct H5. auto. }
Qed.

(** ** matrix_each_assoc *)
(** The matrix addition function has the property of associative law : 
    A + B + C = A + ( B + C ). *)
Lemma matrix_assoc : forall{m n:nat}(left middle right:@Mat A m n ) ,
  (forall a b c: A, add (add a b) c = add a (add b c)) ->  
  matrix_each A add (matrix_each A add left middle) right ===
  matrix_each A add left (matrix_each A add middle right) .
Proof.
  intros m n.
  induction left.
  induction middle.
  induction right.
  intros.
  unfold matrix_each at 2. unfold mat_each. simpl.
  unfold matrix_each at 3. unfold mat_each. simpl.
  unfold matrix_each at 2. unfold mat_each. simpl.
  unfold matrix_each. unfold mat_each. simpl.
  simpl. unfold M_eq. simpl.
  apply matrix_each'_assoc with(n:=n) (m:=m) . auto.
  apply mat_height. apply mat_height0. apply mat_height1.
  apply mat_width. apply mat_width0. apply mat_width1.
Qed.

(** * Zero Matrix Plus Matrix Law *)

(** *** list_add_zero_l *)
(** The addition of zero list and list l : lzero + l = l. *)
Lemma list_add_zero_l : forall n l ,
 ((forall a , add Zero a = a))->length l = n -> 
  list_each A add (list_o A Zero n) l = l.
Proof.
  induction n. induction l.
  - simpl. intros. auto.
  - simpl. intros. inversion H0.
  - intros. simpl. induction l. auto. rewrite H. rewrite IHn;auto.
Qed.

(** *** dlist_add_zero_l *)
(** The addition of zero two-dimensional list and two-dimensional list
    dl: dlzero + dl = dl. *)
Lemma dlist_add_zero_l : forall m n ma , 
  (forall a , add Zero a = a) -> 
  height ma = m -> width ma n -> 
  mat_each' A add (dlist_o A Zero m n) ma = ma.
Proof.
  induction m.
  induction n.
  - simpl. intros. induction ma. auto. inversion H0.
  - simpl. intros. induction ma. auto. inversion H0.
  - induction n. induction ma.
    + simpl. auto.
    + simpl. intros. assert (a=nil). induction a. auto. 
      inversion H1. inversion H2. rewrite H2. rewrite IHm.
      auto. auto. auto. apply H1.
    + induction ma.
      { simpl. auto. }
      { intros. simpl. induction a. inversion H1. inversion H2.
        f_equal. rewrite H. rewrite list_add_zero_l;auto. 
        inversion H1. inversion H2. auto. apply IHm;auto.
        inversion H1. apply H3. }
Qed.

(** *** matrix_add_zero_l *)
(** The addition of Zero matrix and matrix M : O + M = M.*)
Lemma matrix_add_zero_l : forall{m n:nat} (ma:@Mat A m n) ,
  (forall a , add Zero a = a)-> 
    (matrix_each A add (MO A Zero m n) ma) === ma.
Proof.
  intros m n.
  induction ma.
  intros.
  unfold matrix_each.
  unfold M_eq.
  simpl.
  unfold mat_each.
  simpl.
  apply dlist_add_zero_l;auto.
Qed.

(** * Matrix Plus Zero Matrix Law *)

(** *** list_add_zero_r *)
(** The addition of list l and zero list : l + lzero = l. *)
Lemma list_add_zero_r : forall n l , ((forall a , add a Zero = a))->
  length l = n -> list_each A add l (list_o A Zero n) = l.
Proof.
  induction n. induction l.
  - simpl. intros. auto.
  - simpl. intros. inversion H0.
  - intros. simpl. induction l. auto. simpl. rewrite H. rewrite IHn;auto. 
Qed.

(** *** dlist_add_zero_r *)
(** The addition of two-dimensional list dl and zero two-dimensional 
    list : dl + dlzero = dl. *)
Lemma dlist_add_zero_r : forall m n ma ,
   (forall a , add a Zero = a) -> 
  height ma = m -> width ma n -> 
  mat_each' A add ma (dlist_o A Zero m n) = ma.
Proof.
  induction m.
  induction n.
  - simpl. intros. induction ma. auto. inversion H0.
  - simpl. intros. induction ma. auto. inversion H0.
  - induction n. induction ma.
    + simpl. auto.
    + simpl. intros. assert (a=nil). induction a. auto.
      inversion H1. inversion H2. rewrite H2. rewrite IHm.
       auto. auto. auto. apply H1.
    + induction ma.
      { simpl. auto. }
      { intros. simpl. induction a. inversion H1. inversion H2.
        f_equal. simpl. rewrite H. rewrite list_add_zero_r;auto.
        inversion H1. inversion H2. auto. apply IHm;auto. 
        inversion H1. apply H3. }
Qed.

(** ** matrix_add_zero_r *)
(** The addition of matrix M and Zero matrix  : M + O = M.*)
Lemma matrix_add_zero_r : forall {m n:nat} (ma:@Mat A m n) ,
  (forall a , add a Zero = a)->
  (matrix_each A add ma (MO A Zero m n)) === ma.
Proof.
  intros m n.
  induction ma.
  intros.
  unfold matrix_each.
  unfold M_eq.
  simpl.
  unfold mat_each.
  simpl.
  apply dlist_add_zero_r;auto.
  Qed.


End add_lemma.

Lemma list_each_eq: forall (A:Set)f a b c d,
  a= c -> b = d ->
  list_each A f a b = list_each A f c d.
Proof.
  induction a,c. simpl. auto. intros. inversion H.
  intros. inversion H.
  induction b,d. intros. simpl. auto.
  intros. inversion H0. intros. inversion H0.
  intros. simpl. f_equal. f_equal.
  inversion H. auto. inversion H0. auto.
  apply IHa. inversion H. auto. inversion H0. auto.
Qed.

Lemma mat_each'_eq: forall (A:Set)f ma1 ma2 ma3 ma4,
  ma1 = ma3 ->ma2 = ma4 ->
  mat_each' A f ma1 ma2 = mat_each' A f ma3 ma4.
Proof.
  induction ma1. induction ma3. simpl. auto.
  intros. inversion H. induction ma3. intros. inversion H.
  induction ma2. induction ma4. simpl. auto.
  intros. inversion H0. induction ma4.
  intros. inversion H0. intros. simpl.
  f_equal. apply list_each_eq. inversion H.
  auto. inversion H0. auto. apply IHma1.
  inversion H. auto. inversion H0. auto.
Qed.

Lemma matrix_each_compat : 
  forall (A:Set) f m n, 
     forall x x' : (@Mat A m n), @M_eq A m n x x' ->
     forall y y' : (@Mat A m n), @M_eq A m n y y' ->
         @M_eq A m n 
    (matrix_each A f x y) (matrix_each A f x' y').
Proof.
  induction x,x',y,y'. unfold M_eq,matrix_each,mat_each.
  simpl. unfold M_eq in H. simpl in H. intros. 
  apply mat_each'_eq. auto. auto.
Qed.

Add Parametric Morphism {A:Set}{f}{m n :nat}: (matrix_each A f )
  with signature (@M_eq A m n) ==> (@M_eq A m n) ==> (@M_eq A m n) 
  as mat_each_mor.
Proof.
exact (@matrix_each_compat A f m n).
Qed.


Lemma list_map_eq: forall A f a b,
  a = b->
  list_map A f a = list_map A f b.
Proof.
  induction a. intros. rewrite <- H. simpl. auto.
  induction b. intros. inversion H. intros.
  simpl. f_equal. f_equal. inversion H. auto.
  apply IHa. inversion H. auto.
Qed.

Lemma dlist_map_eq: forall A f a b,
  a = b ->
  dlist_map A f a = dlist_map A f b.
Proof.
  induction a. simpl. intros. rewrite <- H. simpl. auto.
  induction b. intros. inversion H.
  intros. simpl. f_equal. apply list_map_eq.
  inversion H. auto. apply IHa. inversion H.
  auto.
Qed.

Lemma matrix_map_compat : 
  forall (A:Set) f m n, 
     forall x x' : (@Mat A m n), @M_eq A m n x x' ->
         @M_eq A m n 
    (matrix_map A f x) (matrix_map A f x').
Proof.
  induction x,x'. unfold M_eq,matrix_map,matrix_map'.
  simpl. intros. apply dlist_map_eq. auto.
Qed.

Add Parametric Morphism {A:Set}{f}{m n :nat}: (matrix_map A f )
  with signature (@M_eq A m n) ==> (@M_eq A m n)
  as mat_map_mor.
Proof.
exact (@matrix_map_compat A f m n).
Qed.


